Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    2nd(cons(X,n__cons(Y,Z)))  → activate(Y)
2:    from(X)  → cons(X,n__from(s(X)))
3:    cons(X1,X2)  → n__cons(X1,X2)
4:    from(X)  → n__from(X)
5:    activate(n__cons(X1,X2))  → cons(X1,X2)
6:    activate(n__from(X))  → from(X)
7:    activate(X)  → X
There are 4 dependency pairs:
8:    2nd#(cons(X,n__cons(Y,Z)))  → ACTIVATE(Y)
9:    FROM(X)  → CONS(X,n__from(s(X)))
10:    ACTIVATE(n__cons(X1,X2))  → CONS(X1,X2)
11:    ACTIVATE(n__from(X))  → FROM(X)
The approximated dependency graph contains no SCCs and hence the TRS is trivially terminating.
Tyrolean Termination Tool  (0.00 seconds)   ---  May 3, 2006